home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / MacHaskell 2.2 / type / expression-typechecking.scm < prev    next >
Encoding:
Text File  |  1994-09-27  |  16.8 KB  |  478 lines  |  [TEXT/CCL2]
  1. ;;; This file contains typecheckers for all expressions except vars and
  2. ;;; declarations.
  3.  
  4. ;;; From valdef-structs:
  5. ;;;   valdef, single-fun-def are in type-decls
  6.  
  7. (define-type-checker guarded-rhs
  8.   (type-check guarded-rhs rhs rhs-type
  9.     (type-check guarded-rhs guard guard-type
  10.       (type-unify guard-type *bool-type*
  11.           (type-mismatch/fixed (guarded-rhs-guard object)
  12.        "Guards must be of type Bool" guard-type))
  13.       (return-type object rhs-type))))
  14.  
  15. ;;; These type checkers deal with patterns.
  16.  
  17. (define-type-checker as-pat
  18.   (type-check as-pat pattern as-type
  19.     (setf (var-type (var-ref-var (as-pat-var object))) as-type)
  20.     (return-type object as-type)))
  21.  
  22. (define-type-checker irr-pat
  23.   (type-check irr-pat pattern pattern-type
  24.     (return-type object pattern-type)))
  25.  
  26. (define-type-checker var-pat
  27.   (fresh-type var-type
  28.     (setf (var-type (var-ref-var (var-pat-var object))) var-type)
  29.     (return-type object var-type)))
  30.  
  31. (define-type-checker wildcard-pat
  32.  (fresh-type pat-type
  33.     (return-type object pat-type)))
  34.  
  35. ;;; Constant patterns create a piece of code to actually to the
  36. ;;; match: ((==) k), where k is the constant.  This code is placed in the
  37. ;;; match-fn slot of the const-pat and is used by the cfn.
  38.  
  39. (define-type-checker const-pat
  40.  (let* ((val (const-pat-value object))
  41.     (match-fn (**app (**var/def (core-symbol "==")) val)))
  42.    (setf (const-pat-match-fn object) match-fn)
  43.    (type-check const-pat match-fn match-type
  44.      (fresh-type res-type
  45.        (type-unify match-type (**arrow res-type *bool-type*) #f)
  46.        (return-type object res-type)))))
  47.  
  48. (define-type-checker plus-pat
  49.   (let* ((kp (**int (plus-pat-k object)))
  50.      (km (**int (- (plus-pat-k object))))
  51.      (match-fn (**app (**var/def (core-symbol "<=")) kp))
  52.      (bind-fn (**app (**var/def (core-symbol "+")) km)))
  53.     (setf (plus-pat-match-fn object) match-fn)
  54.     (setf (plus-pat-bind-fn object) bind-fn)
  55.     (fresh-type res-type
  56.       (setf (ntyvar-context res-type) (list (core-symbol "Integral")))
  57.       (type-check plus-pat match-fn match-type
  58.         (type-check plus-pat bind-fn bind-type
  59.           (type-check plus-pat pattern pat-type
  60.         (type-unify match-type (**arrow pat-type *bool-type*) #f)
  61.         (type-unify bind-type (**arrow pat-type pat-type) #f)
  62.         (type-unify res-type pat-type #f)
  63.         (return-type object res-type)))))))
  64.  
  65. (define-type-checker pcon
  66.  (let ((con (pcon-con object)))
  67.   (if (eqv? (length (pcon-pats object)) (con-arity con))
  68.       (type-check/list pcon pats arg-types
  69.        (fresh-type res-type
  70.         (let ((con-type (instantiate-gtype (con-signature con)))
  71.           (tyvars (list res-type)))
  72.      (dotimes (i (con-arity con))
  73.          (push (**ntyvar) tyvars))
  74.      (type-unify con-type (**arrow/l tyvars) #f)
  75.      (dolist (arg (pcon-pats object))
  76.        (type-unify (car tyvars) (car arg-types)
  77.         (arg-type-mismatch-msg object arg (car arg-types)
  78.                    con (car tyvars) con-type))
  79.        (setf tyvars (cdr tyvars))
  80.        (setf arg-types (cdr arg-types)))
  81.      (return-type object res-type))))
  82.   (begin
  83.     (phase-error 'constructor-arity-mismatch
  84.          "Constructor ~A should have ~A arguments:~%  ~A"
  85.          con (con-arity con) object)
  86.     (type-check/list pcon pats _
  87.       (fresh-type res-type
  88.        (return-type object res-type)))))))
  89.  
  90. (define-type-checker list-pat
  91.   (if (null? (list-pat-pats object))
  92.       (return-type object (instantiate-gtype
  93.                  (algdata-signature (core-symbol "List"))))
  94.       (type-check/unify-list list-pat pats element-type
  95.        (type-mismatch/list object
  96.          "List elements have different types")
  97.     (return-type object (**list-of element-type)))))
  98.  
  99. ;;; These are in the order defined in exp-structs.scm
  100.  
  101. (define-type-checker lambda
  102.  (with-new-tyvars
  103.   (fresh-monomorphic-types (length (lambda-pats object)) arg-vars
  104.     (type-check/list lambda pats arg-types
  105.      (unify-list arg-types arg-vars)
  106.      (type-check lambda body body-type
  107.       (return-type object (**arrow/l-2 arg-vars body-type)))))))
  108.  
  109. (define-type-checker let
  110.   (type-check/decls let decls
  111.     (type-check let body let-type
  112.       (return-type object let-type))))
  113.  
  114. (define-type-checker if
  115.   (type-check if test-exp test-type
  116.     (type-unify test-type *bool-type*
  117.         (type-mismatch/fixed object
  118.      "The test in an if statement must be of type Bool"
  119.      test-type))
  120.     (type-check if then-exp then-type
  121.       (type-check if else-exp else-type
  122.         (type-unify then-type else-type
  123.               (type-mismatch object
  124.            "then and else clauses have different types"
  125.            then-type else-type))
  126.     (return-type object then-type)))))
  127.  
  128. (define-type-checker case
  129.  (add-error-handlers/case object)
  130.  (with-new-tyvars
  131.   (let ((case-exp object))  ; needed since object is rebound later
  132.    (fresh-monomorphic-type arg-type
  133.     (type-check case exp exp-type
  134.       (type-unify arg-type exp-type #f) ; just to make it monomorphic
  135.       (fresh-type res-type
  136.     (dolist (object (case-alts object))
  137.       (recover-type-error ;;; %%% Needs work
  138.        (type-check alt pat pat-type
  139.          (type-unify pat-type arg-type
  140.                 (list
  141.          (list
  142.                    "Conflict in case alternative pattern types.~%~
  143.                     Case alternative: ~A~
  144.                     Type inferred for case selector: ~A~
  145.                     Type inferred for pattern: ~A"
  146.                    (szn object 40) (sznt arg-type 40) (sznt pat-type 40))))
  147.          (type-check/decls alt where-decls
  148.            (type-check/unify-list alt rhs-list rhs-type
  149.                  (type-mismatch/list object
  150.              "Guarded expressions must have the same type")
  151.          (type-unify rhs-type res-type
  152.                   (list
  153.            (list
  154.                      "Conflict in case alternative values.~%~
  155.                       Case alternative: ~A~
  156.                       Type inferred for case result: ~A~
  157.                       Type inferred for this result: ~A"
  158.                     (szn object 60) (sznt res-type 40)
  159.             (sznt rhs-type 40)))))))))
  160.     (return-type case-exp res-type)))))))
  161.  
  162. (define-type-checker bottom
  163.   (return-type (**save-old-exp
  164.         object
  165.         (make-bottom-call object (bottom-context object))) (**ntyvar)))
  166.  
  167. (define (make-bottom-call object context)
  168.  (let ((sp (ast-node-line-number object)))
  169.   (**abort
  170.    (if context
  171.        (format '#f "Call to ~Aaborted, line ~A in file ~A~%"
  172.            (sz (valdef-lhs context) 30)
  173.            (source-pointer-line sp) (source-pointer-file sp))
  174.        (format '#f "_ evaluated at line ~A in file ~A~%"
  175.            (source-pointer-line sp) (source-pointer-file sp))))))
  176.  
  177. ;;; Expressions with signatures are transformed into let expressions
  178. ;;; with signatures.  
  179.  
  180. ;;;    exp :: type   is rewritten as
  181. ;;;    let temp = exp
  182. ;;;        temp :: type
  183. ;;;     in temp
  184.  
  185. (define-type-checker exp-sign
  186.  (type-rewrite
  187.   (let* ((temp-var (create-temp-var "TC"))
  188.      (decl (**valdef (**var-pat/def temp-var) '() (exp-sign-exp object)))
  189.      (let-exp (**let (list decl) (**var/def temp-var)))
  190.      (signature (exp-sign-signature object)))
  191.       (setf (var-signature temp-var)
  192.         (ast->gtype (signature-context signature)
  193.             (signature-type signature)))
  194.       let-exp)))
  195.  
  196. ;;; A number of special constructs have been hacked in using ordinary
  197. ;;; application syntax.  These special applications are recognized here.
  198.  
  199. (define (is-special-app? app)
  200.   (and (var-ref? (app-fn app))
  201.        (let ((var (var-ref-var (app-fn app))))
  202.      (or (eq? var (core-symbol "dictSel"))
  203.          (eq? var (core-symbol "typeOf"))
  204.          (eq? var (core-symbol "toDynamic"))
  205.          (eq? var (core-symbol "fromDynamic"))
  206.          (eq? var (core-symbol "patternMatchError"))))))
  207.  
  208. (define-type-checker app
  209.   (if (var-ref? (app-fn object))
  210.       (let ((var (var-ref-var (app-fn object))))
  211.     (cond ((eq? var (core-symbol "dictSel"))
  212.            (type-check-dict-sel (app-arg object)))
  213.           ((eq? var (core-symbol "typeOf"))
  214.            (type-check-type-of (app-arg object)))
  215.           ((eq? var (core-symbol "toDynamic"))
  216.            (type-check-to-dynamic (app-arg object)))
  217.           ((eq? var (core-symbol "fromDynamic"))
  218.            (type-check-from-dynamic object))
  219.           ((eq? var (core-symbol "patternMatchError"))
  220.            (type-check-pme object))
  221.           (else
  222.            (type-check-ordinary-app object))))
  223.       (type-check-ordinary-app object)))
  224.  
  225. (define (type-check-ordinary-app object)
  226.  (fresh-type res-type
  227.   (mlet ((top-app object)
  228.      ((object args tyvars) (destructure-app object '() (list res-type))))
  229.     (type-check app fn fn-type
  230.       (type-unify fn-type (**arrow/l tyvars)
  231.        (let* ((fn-type-1 (fully-expand-ntype fn-type))
  232.           (arity (count-type-arity fn-type-1)))
  233.         (list
  234.      (list
  235.     "While type checking: ~A~
  236.      The type of function ~Ais inferred as ~A~
  237.      which is ~A"
  238.         (szn top-app 60) (sz (app-fn object) 20) (sznt fn-type-1 40)
  239.     (if (eqv? arity 0)
  240.         "not a function"
  241.         (format '#f "a function of ~A arguments" arity))))))
  242.       (let ((tv1 tyvars))
  243.     (dolist (object args)
  244.       (type-check app arg arg-type
  245.         (type-unify arg-type (car tv1)
  246.           (arg-type-mismatch-msg top-app (app-arg object) arg-type
  247.                      (app-fn (car args)) (car tv1)
  248.                      (fully-expand-ntype fn-type))))
  249.       (setf tv1 (cdr tv1)))))
  250.     (return-type top-app res-type))))
  251.  
  252. (define (arg-type-mismatch-msg top arg arg-type fn i-type fn-type)
  253.  (cons
  254.   (list "While type checking ~A~
  255.          The type of the argument ~Ais inferred as ~A~
  256.          The function ~Arequires an argument of type ~A~
  257.          The typing of this call of ~Ais ~A"
  258.     (szn top 50) (sz arg 20) (sznt arg-type 20)
  259.     (sz fn 20)
  260.     (sznt i-type 20) (sz fn 40)
  261.     (sznt fn-type 25))
  262.   (show-original-type fn)))
  263.  
  264. (define (destructure-app app args tyvars)
  265.   (if (and (app? app) (not (is-special-app? app)))
  266.       (destructure-app (app-fn app) (cons app args) (cons (**ntyvar) tyvars))
  267.       (values (car args) args tyvars)))
  268.  
  269. (define (show-original-type fn)
  270.   (when (is-type? 'save-old-exp fn)
  271.     (setf fn (save-old-exp-old-exp fn)))
  272.   (when (con-ref? fn)
  273.     (setf fn (con-ref-con fn)))
  274.   (cond ((and (var-ref? fn)
  275.           (gtype? (var-type (var-ref-var fn)))
  276.           (not (null? (gtype-context (var-type (var-ref-var fn))))))
  277.      (list
  278.       (list "The signature of ~Ais ~A"
  279.         (sz fn 20) (szn (var-type (var-ref-var fn)) 35))))
  280.     ((and (con? fn)
  281.           (not (null? (gtype-context (con-signature fn)))))
  282.      (list
  283.       (list "The signature of constructor ~Ais ~A"
  284.         (sz fn 20) (szn (con-signature fn) 35))))
  285.     (else '())))
  286.  
  287. ;;; This is a special hack for typing dictionary selection as used in
  288. ;;; generic tuple functions.  This extracts a dictionary from a TupleDict
  289. ;;; object and uses is to resolve the overloading of a designated
  290. ;;; expression.  The expresion must generate exactly one new context.
  291.  
  292. (define (type-check-dict-sel arg)
  293.   (when (or (not (app? arg))
  294.         (not (app? (app-fn arg))))
  295.      (dict-sel-error))
  296.   (let* ((exp (app-fn (app-fn arg)))
  297.      (dict-var (app-arg (app-fn arg)))
  298.      (i (app-arg arg))
  299.      (p (dynamic *placeholders*)))
  300.     (mlet (((object exp-type) (dispatch-type-check exp)))
  301.       ; check for exactly one new context
  302.       (when (or (eq? (dynamic *placeholders*) p)
  303.         (not (eq? (cdr (dynamic *placeholders*)) p)))
  304.      (dict-sel-error))
  305.     (mlet ((placeholder (car (dynamic *placeholders*)))
  306.            (tyvar (placeholder-tyvar placeholder))
  307.            ((dict-var-ast dict-var-type) (dispatch-type-check dict-var))
  308.            ((index-ast index-type) (dispatch-type-check i)))
  309.        (setf (ntyvar-context tyvar) '()) ; prevent context from leaking out
  310.        (setf (dynamic *placeholders*) p)
  311.            (type-unify dict-var-type
  312.               (**ntycon (core-symbol "TupleDicts") '()) #f)
  313.        (type-unify index-type *int-type* #f)
  314.        (cond ((method-placeholder? placeholder)
  315.           (dict-sel-error))  ; I am lazy.  This means that
  316.          ; dictSel must not be passed a method
  317.          (else
  318.           (setf (placeholder-exp placeholder)
  319.             (**app (**var/def (core-symbol "dictSel"))
  320.                    dict-var-ast index-ast))))
  321.        (return-type object exp-type)))))
  322.  
  323. (define (dict-sel-error)
  324.   (fatal-error 'dict-sel-error "Bad dictSel usage."))
  325.  
  326. (define-type-checker con-ref
  327.   (return-type object (instantiate-gtype (con-signature (con-ref-con object)))))
  328.  
  329. (define-type-checker integer-const
  330.   (cond ((const-overloaded? object)
  331.      (setf (const-overloaded? object) '#f)
  332.      (type-rewrite (**fromInteger object)))
  333.     (else
  334.      (return-type object *Integer-type*))))
  335.  
  336. (define-type-checker float-const
  337.   (cond ((const-overloaded? object)
  338.      (setf (const-overloaded? object) '#f)
  339.      (type-rewrite (**fromRational object)))
  340.     (else
  341.      (return-type object *Rational-type*))))
  342.  
  343. (define-type-checker char-const
  344.   (return-type object *char-type*))
  345.  
  346. (define-type-checker string-const
  347.   (return-type object *string-type*))
  348.  
  349. (define-type-checker list-exp
  350.   (if (null? (list-exp-exps object))
  351.       (return-type object (instantiate-gtype
  352.                  (algdata-signature (core-symbol "List"))))
  353.       (type-check/unify-list list-exp exps element-type
  354.           (type-mismatch/list object
  355.          "List elements do not share a common type")
  356.     (return-type object (**list-of element-type)))))
  357.  
  358. (define-type-checker sequence
  359.   (type-rewrite (**enumFrom (sequence-from object))))
  360.  
  361. (define-type-checker sequence-to
  362.   (type-rewrite (**enumFromTo (sequence-to-from object)
  363.                   (sequence-to-to object))))
  364.  
  365. (define-type-checker sequence-then
  366.   (type-rewrite (**enumFromThen (sequence-then-from object)
  367.                 (sequence-then-then object))))
  368.  
  369. (define-type-checker sequence-then-to
  370.   (type-rewrite (**enumFromThenTo (sequence-then-to-from object)
  371.                   (sequence-then-to-then object)
  372.                   (sequence-then-to-to object))))
  373.  
  374. (define-type-checker list-comp
  375.  (with-new-tyvars
  376.   (dolist (object (list-comp-quals object))
  377.     (if (is-type? 'qual-generator object)
  378.     (fresh-type pat-type
  379.      (push pat-type (dynamic *non-generic-tyvars*))
  380.      (type-check qual-generator pat pat-type-1
  381.        (type-unify pat-type pat-type-1 #f)
  382.        (type-check qual-generator exp qual-exp-type
  383.          (type-unify (**list-of pat-type) qual-exp-type
  384.                             (type-mismatch/fixed object
  385.          "Generator expression is not a list" qual-exp-type)))))
  386.      (type-check qual-filter exp filter-type
  387.        (type-unify filter-type *bool-type*
  388.               (type-mismatch/fixed object
  389.         "Filter must have type Bool" filter-type)))))
  390.   (type-check list-comp exp exp-type
  391.      (return-type object (**list-of exp-type)))))
  392.  
  393. (define-type-checker section-l
  394.   (type-check section-l op op-type
  395.     (type-check section-l exp exp-type
  396.       (fresh-type a-type
  397.         (fresh-type b-type
  398.           (fresh-type c-type
  399.             (type-unify op-type (**arrow a-type b-type c-type)
  400.                 (type-mismatch/fixed object
  401.              "Binary function required in section" op-type))
  402.         (type-unify b-type exp-type
  403.                   (type-mismatch object
  404.               "Argument type mismatch" b-type exp-type))
  405.         (return-type object (**arrow a-type c-type))))))))
  406.  
  407. (define-type-checker section-r
  408.   (type-check section-r op op-type
  409.     (type-check section-r exp exp-type
  410.       (fresh-type a-type
  411.         (fresh-type b-type
  412.           (fresh-type c-type
  413.             (type-unify op-type (**arrow a-type b-type c-type)
  414.                   (type-mismatch/fixed object
  415.              "Binary function required" op-type))
  416.         (type-unify exp-type a-type
  417.                     (type-mismatch object
  418.              "Argument type mismatch" a-type exp-type))
  419.         (return-type object (**arrow b-type c-type))))))))
  420.  
  421. (define-type-checker omitted-guard
  422.   (return-type object *bool-type*))
  423.  
  424. (define-type-checker con-number
  425.   (let ((arg-type (instantiate-gtype
  426.            (algdata-signature (con-number-type object)))))
  427.     (type-check con-number value arg-type1
  428.       (type-unify arg-type arg-type1 #f)
  429.       (return-type object *int-type*))))
  430.  
  431. (define-type-checker sel
  432.   (let ((con-type (instantiate-gtype
  433.            (con-signature (sel-constructor object)))))
  434.     (mlet (((res-type exp-type1) (get-ith-type con-type (sel-slot object))))
  435.       (type-check sel value exp-type
  436.         (type-unify exp-type exp-type1 #f)
  437.     (return-type object res-type)))))
  438.  
  439. (define (get-ith-type type i)
  440.  (let ((args (ntycon-args type)))  ; must be an arrow
  441.   (if (eq? i 0)
  442.       (values (car args) (get-ith-type/last (cadr args)))
  443.       (get-ith-type (cadr args) (1- i)))))
  444.  
  445. (define (get-ith-type/last type)
  446.   (if (eq? (ntycon-tycon type) (core-symbol "Arrow"))
  447.       (get-ith-type/last (cadr (ntycon-args type)))
  448.       type))
  449.  
  450. (define-type-checker is-constructor
  451.   (let ((alg-type (instantiate-gtype
  452.            (algdata-signature
  453.             (con-alg (is-constructor-constructor object))))))
  454.     (type-check is-constructor value arg-type
  455.       (type-unify arg-type alg-type #f)
  456.       (return-type object *bool-type*))))
  457.  
  458. (define-type-checker cast
  459.   (type-check cast exp _
  460.     (fresh-type res
  461.       (return-type object res))))
  462.  
  463. ;;; This is used for overloaded methods.  The theory is to avoid supplying
  464. ;;; the context at the class level.  This type checks the variable as if it had
  465. ;;; the supplied signature.
  466.  
  467. (define-type-checker overloaded-var-ref
  468.   (let* ((var (overloaded-var-ref-var object))
  469.      (gtype (overloaded-var-ref-sig object))
  470.      (ovar-type (var-type var)))
  471.     (when (recursive-type? ovar-type)
  472.      (error
  473.       "Implementation error: overloaded method found a recursive type"))
  474.     (mlet (((ntype new-vars) (instantiate-gtype/newvars gtype))
  475.        (object1 (insert-dict-placeholders
  476.              (**var/def var) new-vars object)))
  477.       (return-type object1 ntype))))
  478.